Failed to solve the following constraints:
  _12 (x true) x₁ = f x x₁ : A (blocked on _12)
Unsolved metas at the following locations:
  Issue4134.agda:12,7-8
  Issue4134.agda:15,12-16
